i, x:Id, k:Knd, ds:x:Id fp Type, T:Type, f:(State(ds)TDeclaredType(ds;x)).
Normal(ds)
 Normal(T)
 (isrcv(k)  i = destination(lnk(k)))
 es.@i events of kind k change x to f State(ds) (val:T) 

latex

Definitions	x:A. B(x), P  Q, es.P(es), x:A. B(x), t  T, Prop, x. t(x), x(s)
Lemmas	Reffect wf, R-effect-rule, R-realizes wf, effect-p wf, event system wf, assert wf, isrcv wf, Id wf, ldst wf, lnk wf, normal-type wf, normal-ds wf, decl-state wf, decl-type wf, fpf wf, Knd wf